Nuprl Lemma : R-sub-plus-right3 11,40
A,B,C:es_realizer{i:l}. R-sub{i:l}(A; B)  R-sub{i:l}(A; Rplus(C; B)) 
latex

Definitionst  T, P  Q, x:A. B(x), P  Q, prop{i:l}
Lemmases realizer wf, R-sub wf, R-sub-lemma1

origin